w:World, e:E, i:Id. i = loc(e)  isnull(a(i;time(e))) 

latex

Definitions	t  T, {T}, P  Q, x:A. B(x), SQType(T), Id, s = t, Prop, s ~ t, Atom$n, , Type, x.A(x), x. t(x), 1of(t), 2of(t), a(i;t), isnull(a), b, Void, x:AB(x), False, A, {x:A| B(x) }, E, World, time(e), loc(e)
Lemmas	w-E wf, world wf, assert wf, w-isnull wf, w-a wf, pi2 wf, pi1 wf, nat wf, Id wf, Id sq